Inference at * 1 0 4 2 1 
Iof proof for Lemma eq int cases test:



1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. bb : 
8. (i = j) = bb
9. P(if (i = j) then x else y fi )
10.   Type
11. (i = j)  
12. bb:. ((i = j) = bb)  Type
  P(if (i = j) then x else y fi ) 

latex

 by (\p.let A = get_term_arg `A` p 
 bin let x = get_term_arg `x` p 

 binin let e = get_term_arg `e` p 
 bin 
 biAt (get_term_arg `UH` p) 
 bi(Subst 
 bi(Sub(
 mk_equal_term 
 mk_equa(mk_set_term (dv x) A (mk_equal_term A e x)) 
 mk_equae 
 mk_equax) 

 mk_equax(get_int_arg `i` p + 2)) p) 

latex

 1: .....equality..... NILNIL

 1:   (i = j) = bb
 2: .....wf..... NILNIL

 2: 13. z : {bb:| (i = j) = bb} 
 2:   P(if z then x else y fi )  
 3: 

 3: 9. P(if bb then x else y fi )
 3: 10.   Type
 3: 11. (i = j)  
 3: 12. bb:. ((i = j) = bb)  Type
 3:   P(if (i = j) then x else y fi )
 .

Definitions

{x:A| B(x)} , x:A. B(x), if b then t else f fi , f(a), (i = j), s = t, , , x:AB(x), Type, , t  T